app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, app(XS, YS))
from(X) → cons(X, from(s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(cons(X, XS), cons(Y, YS)) → cons(app(Y, cons(X, nil)), zWadr(XS, YS))
prefix(L) → cons(nil, zWadr(L, prefix(L)))
↳ QTRS
↳ DependencyPairsProof
app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, app(XS, YS))
from(X) → cons(X, from(s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(cons(X, XS), cons(Y, YS)) → cons(app(Y, cons(X, nil)), zWadr(XS, YS))
prefix(L) → cons(nil, zWadr(L, prefix(L)))
PREFIX(L) → ZWADR(L, prefix(L))
ZWADR(cons(X, XS), cons(Y, YS)) → ZWADR(XS, YS)
ZWADR(cons(X, XS), cons(Y, YS)) → APP(Y, cons(X, nil))
PREFIX(L) → PREFIX(L)
APP(cons(X, XS), YS) → APP(XS, YS)
FROM(X) → FROM(s(X))
app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, app(XS, YS))
from(X) → cons(X, from(s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(cons(X, XS), cons(Y, YS)) → cons(app(Y, cons(X, nil)), zWadr(XS, YS))
prefix(L) → cons(nil, zWadr(L, prefix(L)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
PREFIX(L) → ZWADR(L, prefix(L))
ZWADR(cons(X, XS), cons(Y, YS)) → ZWADR(XS, YS)
ZWADR(cons(X, XS), cons(Y, YS)) → APP(Y, cons(X, nil))
PREFIX(L) → PREFIX(L)
APP(cons(X, XS), YS) → APP(XS, YS)
FROM(X) → FROM(s(X))
app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, app(XS, YS))
from(X) → cons(X, from(s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(cons(X, XS), cons(Y, YS)) → cons(app(Y, cons(X, nil)), zWadr(XS, YS))
prefix(L) → cons(nil, zWadr(L, prefix(L)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
FROM(X) → FROM(s(X))
app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, app(XS, YS))
from(X) → cons(X, from(s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(cons(X, XS), cons(Y, YS)) → cons(app(Y, cons(X, nil)), zWadr(XS, YS))
prefix(L) → cons(nil, zWadr(L, prefix(L)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
APP(cons(X, XS), YS) → APP(XS, YS)
app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, app(XS, YS))
from(X) → cons(X, from(s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(cons(X, XS), cons(Y, YS)) → cons(app(Y, cons(X, nil)), zWadr(XS, YS))
prefix(L) → cons(nil, zWadr(L, prefix(L)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
APP(cons(X, XS), YS) → APP(XS, YS)
The value of delta used in the strict ordering is 4.
POL(APP(x1, x2)) = (4)x_1
POL(cons(x1, x2)) = 1 + (4)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, app(XS, YS))
from(X) → cons(X, from(s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(cons(X, XS), cons(Y, YS)) → cons(app(Y, cons(X, nil)), zWadr(XS, YS))
prefix(L) → cons(nil, zWadr(L, prefix(L)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
ZWADR(cons(X, XS), cons(Y, YS)) → ZWADR(XS, YS)
app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, app(XS, YS))
from(X) → cons(X, from(s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(cons(X, XS), cons(Y, YS)) → cons(app(Y, cons(X, nil)), zWadr(XS, YS))
prefix(L) → cons(nil, zWadr(L, prefix(L)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ZWADR(cons(X, XS), cons(Y, YS)) → ZWADR(XS, YS)
The value of delta used in the strict ordering is 3.
POL(cons(x1, x2)) = 1 + (4)x_2
POL(ZWADR(x1, x2)) = (3)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, app(XS, YS))
from(X) → cons(X, from(s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(cons(X, XS), cons(Y, YS)) → cons(app(Y, cons(X, nil)), zWadr(XS, YS))
prefix(L) → cons(nil, zWadr(L, prefix(L)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
PREFIX(L) → PREFIX(L)
app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, app(XS, YS))
from(X) → cons(X, from(s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(cons(X, XS), cons(Y, YS)) → cons(app(Y, cons(X, nil)), zWadr(XS, YS))
prefix(L) → cons(nil, zWadr(L, prefix(L)))